rel_exp(T; R; n)
== if (n = 0) then x,y. x = y else x,y. z:T. ((x R z)  (z rel_exp(T; R; (n - 1)) y)) fi 

---

clarification:

rel_exp(T; R; n)
== if (n = 0) then x,y. x = y  T else x,y. z:T. ((x R z)  (z rel_exp(T; R; (n - 1)) y)) fi 
(recursive) 

latex

Definitions	Y, if b then t else f fi , (i = j), s = t, x.A(x), x:A. B(x), P  Q, x f y, f(a), n - m, #$n
FDL editor aliases	rel_exp, rel_exp